$\forall$$T$:Type, $a$:$T$, ${\it as}$:($T$ List), $i$:$\mathbb{Z}$.
\\[0ex](0 $<$ $i$) $\Rightarrow$ ($i$ $\leq$ $\parallel$${\it as}$$\parallel$) $\Rightarrow$ (cons($a$; ${\it as}$)[$i$] = ${\it as}$[($i$ {-} 1)] $\in$ $T$)